E:Type{i}, T:(IdIdType{i}), pred?:(E(?E)),
info:(E((:Id  Id) + (:(:IdLnk  E)  Id))), when, after:(x:Ide:ET(loc(e),x)),
time:(E).
SESAxioms{i:l}(E; T; pred?; info; when; after; time)  {i'} 

latex

Definitions	t  T, x:A. B(x), f(a), P  Q, <a, b>, {T}, SQType(T), , s ~ t, Atom$n, r - s, r + s, Type, x:AB(x), Unit, left + right, IdLnk, x:A  B(x), , P & Q, first(e), b, A, e < e', sender(e), link(e), rcv?(e), source(l), pred!(e;e'), x,y. t(x;y), SWellFounded(R(x;y)), A c B, destination(l), P  Q, x:A. B(x), SESAxioms{i:l}(E;T;pred?;info;when;after;time), loc(e), pred(e), Id, s = t
Lemmas	ldst wf, strongwellfounded wf, pred! wf, lsrc wf, rcv? wf, link wf, sender wf, cless wf, not wf, assert wf, first wf, rationals wf, IdLnk wf, unit wf, qadd wf, qsub wf, Id sq, pred wf, subtype rel self, loc wf, Id wf